Nuprl Lemma : w-isnull_wf
0,22
postcript
pdf
the_w
:World,
i
:Id,
a
:Action(
i
). isnull(
a
)
latex
Definitions
true
,
false
,
World
,
Action(
i
)
,
isnull(
a
)
,
w
.TA
,
w
.M
,
isl(
x
)
,
,
Action(
dec
)
,
w-action-dec(
TA
;
M
;
i
)
,
x
:
A
.
B
(
x
)
,
t
T
,
Id
Lemmas
Id
wf
,
w-action-dec
wf
,
action
wf
,
world
wf
,
bfalse
wf
,
btrue
wf
origin
the_w:World, i:Id, a:Action(i). isnull(a) 
the_w:World, i:Id, a:Action(i). isnull(a) 
x:A. B(x) T